PRISM
=====
Version: 4.5.dev
Date: Fri Feb 26 16:42:01 CET 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 philosophers-mdp.30.prism philosophers-mdp.30.props --property eat
Parsing model file "philosophers-mdp.30.prism"...
Type: MDP
Modules: phil1 phil2 phil3 phil4 phil5 phil6 phil7 phil8 phil9 phil10 phil11 phil12 phil13 phil14 phil15 phil16 phil17 phil18 phil19 phil20 phil21 phil22 phil23 phil24 phil25 phil26 phil27 phil28 phil29 phil30
Variables: p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30
Parsing properties file "philosophers-mdp.30.props"...
1 property:
(1) "eat": Pmax=? [ F ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9)) ]
---------------------------------------------------------------------
Model checking: "eat": Pmax=? [ F ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9)) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 180 iterations in 84.00 seconds (average 0.466689, setup 0.00)
Time for model construction: 85.59 seconds.
Type: MDP
States: 6.499124097455577E29 (1 initial)
Transitions: 2.512267647378575E31
Choices: 2.2718960732972597E31
Transition matrix: 131260 nodes (3 terminal), 2.512267647378575E31 minterms, vars: 120r/120c/30nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 6 iterations in 0.80 seconds (average 0.133667, setup 0.00)
Prob1E: 7 iterations in 0.34 seconds (average 0.047857, setup 0.00)
yes = 6.499124097455577E29, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 1.177 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 87.143 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.